The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CdtProblem
    ↳3 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 62 ms)
    ↳4 CdtProblem
    ↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳6 CdtProblem
    ↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳8 CdtProblem
    ↳9 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳10 CdtProblem
    ↳11 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳12 CdtProblem
    ↳13 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳14 CdtProblem
    ↳15 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳16 CdtProblem
    ↳17 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳18 CdtProblem
    ↳19 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳20 CdtProblem
↳21 CpxTrsMatchBoundsTAProof (⇔, 0 ms)
↳22 BOUNDS(O(1), O(n^1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

c(c(c(a(x, y)))) → b(c(c(c(c(y)))), x)
c(c(b(c(y), 0))) → a(0, c(c(a(y, 0))))
c(c(a(a(y, 0), x))) → c(y)

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(a(z0, z1)))) → b(c(c(c(c(z1)))), z0)
c(c(b(c(z0), 0))) → a(0, c(c(a(z0, 0))))
c(c(a(a(z0, 0), z1))) → c(z0)
Tuples:

C(c(c(a(z0, z1)))) → c1(C(c(c(c(z1)))), C(c(c(z1))), C(c(z1)), C(z1))
C(c(b(c(z0), 0))) → c2(C(c(a(z0, 0))), C(a(z0, 0)))
C(c(a(a(z0, 0), z1))) → c3(C(z0))
S tuples:

C(c(c(a(z0, z1)))) → c1(C(c(c(c(z1)))), C(c(c(z1))), C(c(z1)), C(z1))
C(c(b(c(z0), 0))) → c2(C(c(a(z0, 0))), C(a(z0, 0)))
C(c(a(a(z0, 0), z1))) → c3(C(z0))
K tuples:none
Defined Rule Symbols:

c

Defined Pair Symbols:

C

Compound Symbols:

c1, c2, c3

(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace C(c(c(a(z0, z1)))) → c1(C(c(c(c(z1)))), C(c(c(z1))), C(c(z1)), C(z1)) by

C(c(c(a(x0, a(z0, z1))))) → c1(C(b(c(c(c(c(z1)))), z0)), C(c(c(a(z0, z1)))), C(c(a(z0, z1))), C(a(z0, z1)))
C(c(c(a(x0, c(a(z0, z1)))))) → c1(C(c(b(c(c(c(c(z1)))), z0))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))), C(c(a(z0, z1))))
C(c(c(a(x0, b(c(z0), 0))))) → c1(C(c(a(0, c(c(a(z0, 0)))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))), C(b(c(z0), 0)))
C(c(c(a(x0, a(a(z0, 0), z1))))) → c1(C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))), C(a(a(z0, 0), z1)))
C(c(c(a(x0, c(c(a(z0, z1))))))) → c1(C(c(c(b(c(c(c(c(z1)))), z0)))), C(c(c(c(c(a(z0, z1)))))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))))
C(c(c(a(x0, c(b(c(z0), 0)))))) → c1(C(c(c(a(0, c(c(a(z0, 0))))))), C(c(c(c(b(c(z0), 0))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(c(c(z0)))), C(c(c(c(a(a(z0, 0), z1))))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(c(a(x0, x1)))) → c1

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(a(z0, z1)))) → b(c(c(c(c(z1)))), z0)
c(c(b(c(z0), 0))) → a(0, c(c(a(z0, 0))))
c(c(a(a(z0, 0), z1))) → c(z0)
Tuples:

C(c(b(c(z0), 0))) → c2(C(c(a(z0, 0))), C(a(z0, 0)))
C(c(a(a(z0, 0), z1))) → c3(C(z0))
C(c(c(a(x0, a(z0, z1))))) → c1(C(b(c(c(c(c(z1)))), z0)), C(c(c(a(z0, z1)))), C(c(a(z0, z1))), C(a(z0, z1)))
C(c(c(a(x0, c(a(z0, z1)))))) → c1(C(c(b(c(c(c(c(z1)))), z0))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))), C(c(a(z0, z1))))
C(c(c(a(x0, b(c(z0), 0))))) → c1(C(c(a(0, c(c(a(z0, 0)))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))), C(b(c(z0), 0)))
C(c(c(a(x0, a(a(z0, 0), z1))))) → c1(C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))), C(a(a(z0, 0), z1)))
C(c(c(a(x0, c(c(a(z0, z1))))))) → c1(C(c(c(b(c(c(c(c(z1)))), z0)))), C(c(c(c(c(a(z0, z1)))))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))))
C(c(c(a(x0, c(b(c(z0), 0)))))) → c1(C(c(c(a(0, c(c(a(z0, 0))))))), C(c(c(c(b(c(z0), 0))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(c(c(z0)))), C(c(c(c(a(a(z0, 0), z1))))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(c(a(x0, x1)))) → c1
S tuples:

C(c(b(c(z0), 0))) → c2(C(c(a(z0, 0))), C(a(z0, 0)))
C(c(a(a(z0, 0), z1))) → c3(C(z0))
C(c(c(a(x0, a(z0, z1))))) → c1(C(b(c(c(c(c(z1)))), z0)), C(c(c(a(z0, z1)))), C(c(a(z0, z1))), C(a(z0, z1)))
C(c(c(a(x0, c(a(z0, z1)))))) → c1(C(c(b(c(c(c(c(z1)))), z0))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))), C(c(a(z0, z1))))
C(c(c(a(x0, b(c(z0), 0))))) → c1(C(c(a(0, c(c(a(z0, 0)))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))), C(b(c(z0), 0)))
C(c(c(a(x0, a(a(z0, 0), z1))))) → c1(C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))), C(a(a(z0, 0), z1)))
C(c(c(a(x0, c(c(a(z0, z1))))))) → c1(C(c(c(b(c(c(c(c(z1)))), z0)))), C(c(c(c(c(a(z0, z1)))))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))))
C(c(c(a(x0, c(b(c(z0), 0)))))) → c1(C(c(c(a(0, c(c(a(z0, 0))))))), C(c(c(c(b(c(z0), 0))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(c(c(z0)))), C(c(c(c(a(a(z0, 0), z1))))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(c(a(x0, x1)))) → c1
K tuples:none
Defined Rule Symbols:

c

Defined Pair Symbols:

C

Compound Symbols:

c2, c3, c1, c1

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

C(c(c(a(x0, x1)))) → c1

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(a(z0, z1)))) → b(c(c(c(c(z1)))), z0)
c(c(b(c(z0), 0))) → a(0, c(c(a(z0, 0))))
c(c(a(a(z0, 0), z1))) → c(z0)
Tuples:

C(c(b(c(z0), 0))) → c2(C(c(a(z0, 0))), C(a(z0, 0)))
C(c(a(a(z0, 0), z1))) → c3(C(z0))
C(c(c(a(x0, a(z0, z1))))) → c1(C(b(c(c(c(c(z1)))), z0)), C(c(c(a(z0, z1)))), C(c(a(z0, z1))), C(a(z0, z1)))
C(c(c(a(x0, c(a(z0, z1)))))) → c1(C(c(b(c(c(c(c(z1)))), z0))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))), C(c(a(z0, z1))))
C(c(c(a(x0, b(c(z0), 0))))) → c1(C(c(a(0, c(c(a(z0, 0)))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))), C(b(c(z0), 0)))
C(c(c(a(x0, a(a(z0, 0), z1))))) → c1(C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))), C(a(a(z0, 0), z1)))
C(c(c(a(x0, c(c(a(z0, z1))))))) → c1(C(c(c(b(c(c(c(c(z1)))), z0)))), C(c(c(c(c(a(z0, z1)))))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))))
C(c(c(a(x0, c(b(c(z0), 0)))))) → c1(C(c(c(a(0, c(c(a(z0, 0))))))), C(c(c(c(b(c(z0), 0))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(c(c(z0)))), C(c(c(c(a(a(z0, 0), z1))))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
S tuples:

C(c(b(c(z0), 0))) → c2(C(c(a(z0, 0))), C(a(z0, 0)))
C(c(a(a(z0, 0), z1))) → c3(C(z0))
C(c(c(a(x0, a(z0, z1))))) → c1(C(b(c(c(c(c(z1)))), z0)), C(c(c(a(z0, z1)))), C(c(a(z0, z1))), C(a(z0, z1)))
C(c(c(a(x0, c(a(z0, z1)))))) → c1(C(c(b(c(c(c(c(z1)))), z0))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))), C(c(a(z0, z1))))
C(c(c(a(x0, b(c(z0), 0))))) → c1(C(c(a(0, c(c(a(z0, 0)))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))), C(b(c(z0), 0)))
C(c(c(a(x0, a(a(z0, 0), z1))))) → c1(C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))), C(a(a(z0, 0), z1)))
C(c(c(a(x0, c(c(a(z0, z1))))))) → c1(C(c(c(b(c(c(c(c(z1)))), z0)))), C(c(c(c(c(a(z0, z1)))))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))))
C(c(c(a(x0, c(b(c(z0), 0)))))) → c1(C(c(c(a(0, c(c(a(z0, 0))))))), C(c(c(c(b(c(z0), 0))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(c(c(z0)))), C(c(c(c(a(a(z0, 0), z1))))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
K tuples:none
Defined Rule Symbols:

c

Defined Pair Symbols:

C

Compound Symbols:

c2, c3, c1

(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace C(c(b(c(z0), 0))) → c2(C(c(a(z0, 0))), C(a(z0, 0))) by

C(c(b(c(x0), 0))) → c2(C(c(a(x0, 0))))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(a(z0, z1)))) → b(c(c(c(c(z1)))), z0)
c(c(b(c(z0), 0))) → a(0, c(c(a(z0, 0))))
c(c(a(a(z0, 0), z1))) → c(z0)
Tuples:

C(c(a(a(z0, 0), z1))) → c3(C(z0))
C(c(c(a(x0, a(z0, z1))))) → c1(C(b(c(c(c(c(z1)))), z0)), C(c(c(a(z0, z1)))), C(c(a(z0, z1))), C(a(z0, z1)))
C(c(c(a(x0, c(a(z0, z1)))))) → c1(C(c(b(c(c(c(c(z1)))), z0))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))), C(c(a(z0, z1))))
C(c(c(a(x0, b(c(z0), 0))))) → c1(C(c(a(0, c(c(a(z0, 0)))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))), C(b(c(z0), 0)))
C(c(c(a(x0, a(a(z0, 0), z1))))) → c1(C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))), C(a(a(z0, 0), z1)))
C(c(c(a(x0, c(c(a(z0, z1))))))) → c1(C(c(c(b(c(c(c(c(z1)))), z0)))), C(c(c(c(c(a(z0, z1)))))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))))
C(c(c(a(x0, c(b(c(z0), 0)))))) → c1(C(c(c(a(0, c(c(a(z0, 0))))))), C(c(c(c(b(c(z0), 0))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(c(c(z0)))), C(c(c(c(a(a(z0, 0), z1))))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(b(c(x0), 0))) → c2(C(c(a(x0, 0))))
S tuples:

C(c(a(a(z0, 0), z1))) → c3(C(z0))
C(c(c(a(x0, a(z0, z1))))) → c1(C(b(c(c(c(c(z1)))), z0)), C(c(c(a(z0, z1)))), C(c(a(z0, z1))), C(a(z0, z1)))
C(c(c(a(x0, c(a(z0, z1)))))) → c1(C(c(b(c(c(c(c(z1)))), z0))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))), C(c(a(z0, z1))))
C(c(c(a(x0, b(c(z0), 0))))) → c1(C(c(a(0, c(c(a(z0, 0)))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))), C(b(c(z0), 0)))
C(c(c(a(x0, a(a(z0, 0), z1))))) → c1(C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))), C(a(a(z0, 0), z1)))
C(c(c(a(x0, c(c(a(z0, z1))))))) → c1(C(c(c(b(c(c(c(c(z1)))), z0)))), C(c(c(c(c(a(z0, z1)))))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))))
C(c(c(a(x0, c(b(c(z0), 0)))))) → c1(C(c(c(a(0, c(c(a(z0, 0))))))), C(c(c(c(b(c(z0), 0))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(c(c(z0)))), C(c(c(c(a(a(z0, 0), z1))))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(b(c(x0), 0))) → c2(C(c(a(x0, 0))))
K tuples:none
Defined Rule Symbols:

c

Defined Pair Symbols:

C

Compound Symbols:

c3, c1, c2

(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace C(c(c(a(x0, a(z0, z1))))) → c1(C(b(c(c(c(c(z1)))), z0)), C(c(c(a(z0, z1)))), C(c(a(z0, z1))), C(a(z0, z1))) by

C(c(c(a(x0, a(x1, a(z0, z1)))))) → c1(C(b(c(b(c(c(c(c(z1)))), z0)), x1)), C(c(c(a(x1, a(z0, z1))))), C(c(a(x1, a(z0, z1)))), C(a(x1, a(z0, z1))))
C(c(c(a(x0, a(x1, c(a(z0, z1))))))) → c1(C(b(c(c(b(c(c(c(c(z1)))), z0))), x1)), C(c(c(a(x1, c(a(z0, z1)))))), C(c(a(x1, c(a(z0, z1))))), C(a(x1, c(a(z0, z1)))))
C(c(c(a(x0, a(x1, b(c(z0), 0)))))) → c1(C(b(c(c(a(0, c(c(a(z0, 0)))))), x1)), C(c(c(a(x1, b(c(z0), 0))))), C(c(a(x1, b(c(z0), 0)))), C(a(x1, b(c(z0), 0))))
C(c(c(a(x0, a(x1, a(a(z0, 0), z1)))))) → c1(C(b(c(c(c(z0))), x1)), C(c(c(a(x1, a(a(z0, 0), z1))))), C(c(a(x1, a(a(z0, 0), z1)))), C(a(x1, a(a(z0, 0), z1))))
C(c(c(a(x0, a(x1, c(c(a(z0, z1)))))))) → c1(C(b(c(c(c(b(c(c(c(c(z1)))), z0)))), x1)), C(c(c(a(x1, c(c(a(z0, z1))))))), C(c(a(x1, c(c(a(z0, z1)))))), C(a(x1, c(c(a(z0, z1))))))
C(c(c(a(x0, a(x1, c(b(c(z0), 0))))))) → c1(C(b(c(c(c(a(0, c(c(a(z0, 0))))))), x1)), C(c(c(a(x1, c(b(c(z0), 0)))))), C(c(a(x1, c(b(c(z0), 0))))), C(a(x1, c(b(c(z0), 0)))))
C(c(c(a(x0, a(x1, c(a(a(z0, 0), z1))))))) → c1(C(b(c(c(c(c(z0)))), x1)), C(c(c(a(x1, c(a(a(z0, 0), z1)))))), C(c(a(x1, c(a(a(z0, 0), z1))))), C(a(x1, c(a(a(z0, 0), z1)))))
C(c(c(a(x0, a(x1, x2))))) → c1(C(c(c(a(x1, x2)))), C(c(a(x1, x2))))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(a(z0, z1)))) → b(c(c(c(c(z1)))), z0)
c(c(b(c(z0), 0))) → a(0, c(c(a(z0, 0))))
c(c(a(a(z0, 0), z1))) → c(z0)
Tuples:

C(c(a(a(z0, 0), z1))) → c3(C(z0))
C(c(c(a(x0, c(a(z0, z1)))))) → c1(C(c(b(c(c(c(c(z1)))), z0))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))), C(c(a(z0, z1))))
C(c(c(a(x0, b(c(z0), 0))))) → c1(C(c(a(0, c(c(a(z0, 0)))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))), C(b(c(z0), 0)))
C(c(c(a(x0, a(a(z0, 0), z1))))) → c1(C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))), C(a(a(z0, 0), z1)))
C(c(c(a(x0, c(c(a(z0, z1))))))) → c1(C(c(c(b(c(c(c(c(z1)))), z0)))), C(c(c(c(c(a(z0, z1)))))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))))
C(c(c(a(x0, c(b(c(z0), 0)))))) → c1(C(c(c(a(0, c(c(a(z0, 0))))))), C(c(c(c(b(c(z0), 0))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(c(c(z0)))), C(c(c(c(a(a(z0, 0), z1))))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(b(c(x0), 0))) → c2(C(c(a(x0, 0))))
C(c(c(a(x0, a(x1, a(z0, z1)))))) → c1(C(b(c(b(c(c(c(c(z1)))), z0)), x1)), C(c(c(a(x1, a(z0, z1))))), C(c(a(x1, a(z0, z1)))), C(a(x1, a(z0, z1))))
C(c(c(a(x0, a(x1, c(a(z0, z1))))))) → c1(C(b(c(c(b(c(c(c(c(z1)))), z0))), x1)), C(c(c(a(x1, c(a(z0, z1)))))), C(c(a(x1, c(a(z0, z1))))), C(a(x1, c(a(z0, z1)))))
C(c(c(a(x0, a(x1, b(c(z0), 0)))))) → c1(C(b(c(c(a(0, c(c(a(z0, 0)))))), x1)), C(c(c(a(x1, b(c(z0), 0))))), C(c(a(x1, b(c(z0), 0)))), C(a(x1, b(c(z0), 0))))
C(c(c(a(x0, a(x1, a(a(z0, 0), z1)))))) → c1(C(b(c(c(c(z0))), x1)), C(c(c(a(x1, a(a(z0, 0), z1))))), C(c(a(x1, a(a(z0, 0), z1)))), C(a(x1, a(a(z0, 0), z1))))
C(c(c(a(x0, a(x1, c(c(a(z0, z1)))))))) → c1(C(b(c(c(c(b(c(c(c(c(z1)))), z0)))), x1)), C(c(c(a(x1, c(c(a(z0, z1))))))), C(c(a(x1, c(c(a(z0, z1)))))), C(a(x1, c(c(a(z0, z1))))))
C(c(c(a(x0, a(x1, c(b(c(z0), 0))))))) → c1(C(b(c(c(c(a(0, c(c(a(z0, 0))))))), x1)), C(c(c(a(x1, c(b(c(z0), 0)))))), C(c(a(x1, c(b(c(z0), 0))))), C(a(x1, c(b(c(z0), 0)))))
C(c(c(a(x0, a(x1, c(a(a(z0, 0), z1))))))) → c1(C(b(c(c(c(c(z0)))), x1)), C(c(c(a(x1, c(a(a(z0, 0), z1)))))), C(c(a(x1, c(a(a(z0, 0), z1))))), C(a(x1, c(a(a(z0, 0), z1)))))
C(c(c(a(x0, a(x1, x2))))) → c1(C(c(c(a(x1, x2)))), C(c(a(x1, x2))))
S tuples:

C(c(a(a(z0, 0), z1))) → c3(C(z0))
C(c(c(a(x0, c(a(z0, z1)))))) → c1(C(c(b(c(c(c(c(z1)))), z0))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))), C(c(a(z0, z1))))
C(c(c(a(x0, b(c(z0), 0))))) → c1(C(c(a(0, c(c(a(z0, 0)))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))), C(b(c(z0), 0)))
C(c(c(a(x0, a(a(z0, 0), z1))))) → c1(C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))), C(a(a(z0, 0), z1)))
C(c(c(a(x0, c(c(a(z0, z1))))))) → c1(C(c(c(b(c(c(c(c(z1)))), z0)))), C(c(c(c(c(a(z0, z1)))))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))))
C(c(c(a(x0, c(b(c(z0), 0)))))) → c1(C(c(c(a(0, c(c(a(z0, 0))))))), C(c(c(c(b(c(z0), 0))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(c(c(z0)))), C(c(c(c(a(a(z0, 0), z1))))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(b(c(x0), 0))) → c2(C(c(a(x0, 0))))
C(c(c(a(x0, a(x1, a(z0, z1)))))) → c1(C(b(c(b(c(c(c(c(z1)))), z0)), x1)), C(c(c(a(x1, a(z0, z1))))), C(c(a(x1, a(z0, z1)))), C(a(x1, a(z0, z1))))
C(c(c(a(x0, a(x1, c(a(z0, z1))))))) → c1(C(b(c(c(b(c(c(c(c(z1)))), z0))), x1)), C(c(c(a(x1, c(a(z0, z1)))))), C(c(a(x1, c(a(z0, z1))))), C(a(x1, c(a(z0, z1)))))
C(c(c(a(x0, a(x1, b(c(z0), 0)))))) → c1(C(b(c(c(a(0, c(c(a(z0, 0)))))), x1)), C(c(c(a(x1, b(c(z0), 0))))), C(c(a(x1, b(c(z0), 0)))), C(a(x1, b(c(z0), 0))))
C(c(c(a(x0, a(x1, a(a(z0, 0), z1)))))) → c1(C(b(c(c(c(z0))), x1)), C(c(c(a(x1, a(a(z0, 0), z1))))), C(c(a(x1, a(a(z0, 0), z1)))), C(a(x1, a(a(z0, 0), z1))))
C(c(c(a(x0, a(x1, c(c(a(z0, z1)))))))) → c1(C(b(c(c(c(b(c(c(c(c(z1)))), z0)))), x1)), C(c(c(a(x1, c(c(a(z0, z1))))))), C(c(a(x1, c(c(a(z0, z1)))))), C(a(x1, c(c(a(z0, z1))))))
C(c(c(a(x0, a(x1, c(b(c(z0), 0))))))) → c1(C(b(c(c(c(a(0, c(c(a(z0, 0))))))), x1)), C(c(c(a(x1, c(b(c(z0), 0)))))), C(c(a(x1, c(b(c(z0), 0))))), C(a(x1, c(b(c(z0), 0)))))
C(c(c(a(x0, a(x1, c(a(a(z0, 0), z1))))))) → c1(C(b(c(c(c(c(z0)))), x1)), C(c(c(a(x1, c(a(a(z0, 0), z1)))))), C(c(a(x1, c(a(a(z0, 0), z1))))), C(a(x1, c(a(a(z0, 0), z1)))))
C(c(c(a(x0, a(x1, x2))))) → c1(C(c(c(a(x1, x2)))), C(c(a(x1, x2))))
K tuples:none
Defined Rule Symbols:

c

Defined Pair Symbols:

C

Compound Symbols:

c3, c1, c2, c1

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace C(c(c(a(x0, c(a(z0, z1)))))) → c1(C(c(b(c(c(c(c(z1)))), z0))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))), C(c(a(z0, z1)))) by

C(c(c(a(x0, c(a(z0, z1)))))) → c1(C(c(b(c(c(c(c(z1)))), z0))), C(b(c(c(c(c(z1)))), z0)), C(c(c(a(z0, z1)))), C(c(a(z0, z1))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(b(c(c(c(c(z1)))), a(z0, 0)))), C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(c(a(x0, c(a(x1, x2)))))) → c1(C(c(b(c(c(c(c(x2)))), x1))))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(a(z0, z1)))) → b(c(c(c(c(z1)))), z0)
c(c(b(c(z0), 0))) → a(0, c(c(a(z0, 0))))
c(c(a(a(z0, 0), z1))) → c(z0)
Tuples:

C(c(a(a(z0, 0), z1))) → c3(C(z0))
C(c(c(a(x0, b(c(z0), 0))))) → c1(C(c(a(0, c(c(a(z0, 0)))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))), C(b(c(z0), 0)))
C(c(c(a(x0, a(a(z0, 0), z1))))) → c1(C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))), C(a(a(z0, 0), z1)))
C(c(c(a(x0, c(c(a(z0, z1))))))) → c1(C(c(c(b(c(c(c(c(z1)))), z0)))), C(c(c(c(c(a(z0, z1)))))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))))
C(c(c(a(x0, c(b(c(z0), 0)))))) → c1(C(c(c(a(0, c(c(a(z0, 0))))))), C(c(c(c(b(c(z0), 0))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(c(c(z0)))), C(c(c(c(a(a(z0, 0), z1))))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(b(c(x0), 0))) → c2(C(c(a(x0, 0))))
C(c(c(a(x0, a(x1, a(z0, z1)))))) → c1(C(b(c(b(c(c(c(c(z1)))), z0)), x1)), C(c(c(a(x1, a(z0, z1))))), C(c(a(x1, a(z0, z1)))), C(a(x1, a(z0, z1))))
C(c(c(a(x0, a(x1, c(a(z0, z1))))))) → c1(C(b(c(c(b(c(c(c(c(z1)))), z0))), x1)), C(c(c(a(x1, c(a(z0, z1)))))), C(c(a(x1, c(a(z0, z1))))), C(a(x1, c(a(z0, z1)))))
C(c(c(a(x0, a(x1, b(c(z0), 0)))))) → c1(C(b(c(c(a(0, c(c(a(z0, 0)))))), x1)), C(c(c(a(x1, b(c(z0), 0))))), C(c(a(x1, b(c(z0), 0)))), C(a(x1, b(c(z0), 0))))
C(c(c(a(x0, a(x1, a(a(z0, 0), z1)))))) → c1(C(b(c(c(c(z0))), x1)), C(c(c(a(x1, a(a(z0, 0), z1))))), C(c(a(x1, a(a(z0, 0), z1)))), C(a(x1, a(a(z0, 0), z1))))
C(c(c(a(x0, a(x1, c(c(a(z0, z1)))))))) → c1(C(b(c(c(c(b(c(c(c(c(z1)))), z0)))), x1)), C(c(c(a(x1, c(c(a(z0, z1))))))), C(c(a(x1, c(c(a(z0, z1)))))), C(a(x1, c(c(a(z0, z1))))))
C(c(c(a(x0, a(x1, c(b(c(z0), 0))))))) → c1(C(b(c(c(c(a(0, c(c(a(z0, 0))))))), x1)), C(c(c(a(x1, c(b(c(z0), 0)))))), C(c(a(x1, c(b(c(z0), 0))))), C(a(x1, c(b(c(z0), 0)))))
C(c(c(a(x0, a(x1, c(a(a(z0, 0), z1))))))) → c1(C(b(c(c(c(c(z0)))), x1)), C(c(c(a(x1, c(a(a(z0, 0), z1)))))), C(c(a(x1, c(a(a(z0, 0), z1))))), C(a(x1, c(a(a(z0, 0), z1)))))
C(c(c(a(x0, a(x1, x2))))) → c1(C(c(c(a(x1, x2)))), C(c(a(x1, x2))))
C(c(c(a(x0, c(a(z0, z1)))))) → c1(C(c(b(c(c(c(c(z1)))), z0))), C(b(c(c(c(c(z1)))), z0)), C(c(c(a(z0, z1)))), C(c(a(z0, z1))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(b(c(c(c(c(z1)))), a(z0, 0)))), C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(c(a(x0, c(a(x1, x2)))))) → c1(C(c(b(c(c(c(c(x2)))), x1))))
S tuples:

C(c(a(a(z0, 0), z1))) → c3(C(z0))
C(c(c(a(x0, b(c(z0), 0))))) → c1(C(c(a(0, c(c(a(z0, 0)))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))), C(b(c(z0), 0)))
C(c(c(a(x0, a(a(z0, 0), z1))))) → c1(C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))), C(a(a(z0, 0), z1)))
C(c(c(a(x0, c(c(a(z0, z1))))))) → c1(C(c(c(b(c(c(c(c(z1)))), z0)))), C(c(c(c(c(a(z0, z1)))))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))))
C(c(c(a(x0, c(b(c(z0), 0)))))) → c1(C(c(c(a(0, c(c(a(z0, 0))))))), C(c(c(c(b(c(z0), 0))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(c(c(z0)))), C(c(c(c(a(a(z0, 0), z1))))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(b(c(x0), 0))) → c2(C(c(a(x0, 0))))
C(c(c(a(x0, a(x1, a(z0, z1)))))) → c1(C(b(c(b(c(c(c(c(z1)))), z0)), x1)), C(c(c(a(x1, a(z0, z1))))), C(c(a(x1, a(z0, z1)))), C(a(x1, a(z0, z1))))
C(c(c(a(x0, a(x1, c(a(z0, z1))))))) → c1(C(b(c(c(b(c(c(c(c(z1)))), z0))), x1)), C(c(c(a(x1, c(a(z0, z1)))))), C(c(a(x1, c(a(z0, z1))))), C(a(x1, c(a(z0, z1)))))
C(c(c(a(x0, a(x1, b(c(z0), 0)))))) → c1(C(b(c(c(a(0, c(c(a(z0, 0)))))), x1)), C(c(c(a(x1, b(c(z0), 0))))), C(c(a(x1, b(c(z0), 0)))), C(a(x1, b(c(z0), 0))))
C(c(c(a(x0, a(x1, a(a(z0, 0), z1)))))) → c1(C(b(c(c(c(z0))), x1)), C(c(c(a(x1, a(a(z0, 0), z1))))), C(c(a(x1, a(a(z0, 0), z1)))), C(a(x1, a(a(z0, 0), z1))))
C(c(c(a(x0, a(x1, c(c(a(z0, z1)))))))) → c1(C(b(c(c(c(b(c(c(c(c(z1)))), z0)))), x1)), C(c(c(a(x1, c(c(a(z0, z1))))))), C(c(a(x1, c(c(a(z0, z1)))))), C(a(x1, c(c(a(z0, z1))))))
C(c(c(a(x0, a(x1, c(b(c(z0), 0))))))) → c1(C(b(c(c(c(a(0, c(c(a(z0, 0))))))), x1)), C(c(c(a(x1, c(b(c(z0), 0)))))), C(c(a(x1, c(b(c(z0), 0))))), C(a(x1, c(b(c(z0), 0)))))
C(c(c(a(x0, a(x1, c(a(a(z0, 0), z1))))))) → c1(C(b(c(c(c(c(z0)))), x1)), C(c(c(a(x1, c(a(a(z0, 0), z1)))))), C(c(a(x1, c(a(a(z0, 0), z1))))), C(a(x1, c(a(a(z0, 0), z1)))))
C(c(c(a(x0, a(x1, x2))))) → c1(C(c(c(a(x1, x2)))), C(c(a(x1, x2))))
C(c(c(a(x0, c(a(z0, z1)))))) → c1(C(c(b(c(c(c(c(z1)))), z0))), C(b(c(c(c(c(z1)))), z0)), C(c(c(a(z0, z1)))), C(c(a(z0, z1))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(b(c(c(c(c(z1)))), a(z0, 0)))), C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(c(a(x0, c(a(x1, x2)))))) → c1(C(c(b(c(c(c(c(x2)))), x1))))
K tuples:none
Defined Rule Symbols:

c

Defined Pair Symbols:

C

Compound Symbols:

c3, c1, c2, c1, c1

(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace C(c(c(a(x0, b(c(z0), 0))))) → c1(C(c(a(0, c(c(a(z0, 0)))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))), C(b(c(z0), 0))) by

C(c(c(a(x0, b(c(a(z0, 0)), 0))))) → c1(C(c(a(0, c(z0)))), C(c(c(b(c(a(z0, 0)), 0)))), C(c(b(c(a(z0, 0)), 0))), C(b(c(a(z0, 0)), 0)))
C(c(c(a(x0, b(c(x1), 0))))) → c1(C(c(c(b(c(x1), 0)))), C(c(b(c(x1), 0))))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(a(z0, z1)))) → b(c(c(c(c(z1)))), z0)
c(c(b(c(z0), 0))) → a(0, c(c(a(z0, 0))))
c(c(a(a(z0, 0), z1))) → c(z0)
Tuples:

C(c(a(a(z0, 0), z1))) → c3(C(z0))
C(c(c(a(x0, a(a(z0, 0), z1))))) → c1(C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))), C(a(a(z0, 0), z1)))
C(c(c(a(x0, c(c(a(z0, z1))))))) → c1(C(c(c(b(c(c(c(c(z1)))), z0)))), C(c(c(c(c(a(z0, z1)))))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))))
C(c(c(a(x0, c(b(c(z0), 0)))))) → c1(C(c(c(a(0, c(c(a(z0, 0))))))), C(c(c(c(b(c(z0), 0))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(c(c(z0)))), C(c(c(c(a(a(z0, 0), z1))))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(b(c(x0), 0))) → c2(C(c(a(x0, 0))))
C(c(c(a(x0, a(x1, a(z0, z1)))))) → c1(C(b(c(b(c(c(c(c(z1)))), z0)), x1)), C(c(c(a(x1, a(z0, z1))))), C(c(a(x1, a(z0, z1)))), C(a(x1, a(z0, z1))))
C(c(c(a(x0, a(x1, c(a(z0, z1))))))) → c1(C(b(c(c(b(c(c(c(c(z1)))), z0))), x1)), C(c(c(a(x1, c(a(z0, z1)))))), C(c(a(x1, c(a(z0, z1))))), C(a(x1, c(a(z0, z1)))))
C(c(c(a(x0, a(x1, b(c(z0), 0)))))) → c1(C(b(c(c(a(0, c(c(a(z0, 0)))))), x1)), C(c(c(a(x1, b(c(z0), 0))))), C(c(a(x1, b(c(z0), 0)))), C(a(x1, b(c(z0), 0))))
C(c(c(a(x0, a(x1, a(a(z0, 0), z1)))))) → c1(C(b(c(c(c(z0))), x1)), C(c(c(a(x1, a(a(z0, 0), z1))))), C(c(a(x1, a(a(z0, 0), z1)))), C(a(x1, a(a(z0, 0), z1))))
C(c(c(a(x0, a(x1, c(c(a(z0, z1)))))))) → c1(C(b(c(c(c(b(c(c(c(c(z1)))), z0)))), x1)), C(c(c(a(x1, c(c(a(z0, z1))))))), C(c(a(x1, c(c(a(z0, z1)))))), C(a(x1, c(c(a(z0, z1))))))
C(c(c(a(x0, a(x1, c(b(c(z0), 0))))))) → c1(C(b(c(c(c(a(0, c(c(a(z0, 0))))))), x1)), C(c(c(a(x1, c(b(c(z0), 0)))))), C(c(a(x1, c(b(c(z0), 0))))), C(a(x1, c(b(c(z0), 0)))))
C(c(c(a(x0, a(x1, c(a(a(z0, 0), z1))))))) → c1(C(b(c(c(c(c(z0)))), x1)), C(c(c(a(x1, c(a(a(z0, 0), z1)))))), C(c(a(x1, c(a(a(z0, 0), z1))))), C(a(x1, c(a(a(z0, 0), z1)))))
C(c(c(a(x0, a(x1, x2))))) → c1(C(c(c(a(x1, x2)))), C(c(a(x1, x2))))
C(c(c(a(x0, c(a(z0, z1)))))) → c1(C(c(b(c(c(c(c(z1)))), z0))), C(b(c(c(c(c(z1)))), z0)), C(c(c(a(z0, z1)))), C(c(a(z0, z1))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(b(c(c(c(c(z1)))), a(z0, 0)))), C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(c(a(x0, c(a(x1, x2)))))) → c1(C(c(b(c(c(c(c(x2)))), x1))))
C(c(c(a(x0, b(c(a(z0, 0)), 0))))) → c1(C(c(a(0, c(z0)))), C(c(c(b(c(a(z0, 0)), 0)))), C(c(b(c(a(z0, 0)), 0))), C(b(c(a(z0, 0)), 0)))
C(c(c(a(x0, b(c(x1), 0))))) → c1(C(c(c(b(c(x1), 0)))), C(c(b(c(x1), 0))))
S tuples:

C(c(a(a(z0, 0), z1))) → c3(C(z0))
C(c(c(a(x0, a(a(z0, 0), z1))))) → c1(C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))), C(a(a(z0, 0), z1)))
C(c(c(a(x0, c(c(a(z0, z1))))))) → c1(C(c(c(b(c(c(c(c(z1)))), z0)))), C(c(c(c(c(a(z0, z1)))))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))))
C(c(c(a(x0, c(b(c(z0), 0)))))) → c1(C(c(c(a(0, c(c(a(z0, 0))))))), C(c(c(c(b(c(z0), 0))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(c(c(z0)))), C(c(c(c(a(a(z0, 0), z1))))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(b(c(x0), 0))) → c2(C(c(a(x0, 0))))
C(c(c(a(x0, a(x1, a(z0, z1)))))) → c1(C(b(c(b(c(c(c(c(z1)))), z0)), x1)), C(c(c(a(x1, a(z0, z1))))), C(c(a(x1, a(z0, z1)))), C(a(x1, a(z0, z1))))
C(c(c(a(x0, a(x1, c(a(z0, z1))))))) → c1(C(b(c(c(b(c(c(c(c(z1)))), z0))), x1)), C(c(c(a(x1, c(a(z0, z1)))))), C(c(a(x1, c(a(z0, z1))))), C(a(x1, c(a(z0, z1)))))
C(c(c(a(x0, a(x1, b(c(z0), 0)))))) → c1(C(b(c(c(a(0, c(c(a(z0, 0)))))), x1)), C(c(c(a(x1, b(c(z0), 0))))), C(c(a(x1, b(c(z0), 0)))), C(a(x1, b(c(z0), 0))))
C(c(c(a(x0, a(x1, a(a(z0, 0), z1)))))) → c1(C(b(c(c(c(z0))), x1)), C(c(c(a(x1, a(a(z0, 0), z1))))), C(c(a(x1, a(a(z0, 0), z1)))), C(a(x1, a(a(z0, 0), z1))))
C(c(c(a(x0, a(x1, c(c(a(z0, z1)))))))) → c1(C(b(c(c(c(b(c(c(c(c(z1)))), z0)))), x1)), C(c(c(a(x1, c(c(a(z0, z1))))))), C(c(a(x1, c(c(a(z0, z1)))))), C(a(x1, c(c(a(z0, z1))))))
C(c(c(a(x0, a(x1, c(b(c(z0), 0))))))) → c1(C(b(c(c(c(a(0, c(c(a(z0, 0))))))), x1)), C(c(c(a(x1, c(b(c(z0), 0)))))), C(c(a(x1, c(b(c(z0), 0))))), C(a(x1, c(b(c(z0), 0)))))
C(c(c(a(x0, a(x1, c(a(a(z0, 0), z1))))))) → c1(C(b(c(c(c(c(z0)))), x1)), C(c(c(a(x1, c(a(a(z0, 0), z1)))))), C(c(a(x1, c(a(a(z0, 0), z1))))), C(a(x1, c(a(a(z0, 0), z1)))))
C(c(c(a(x0, a(x1, x2))))) → c1(C(c(c(a(x1, x2)))), C(c(a(x1, x2))))
C(c(c(a(x0, c(a(z0, z1)))))) → c1(C(c(b(c(c(c(c(z1)))), z0))), C(b(c(c(c(c(z1)))), z0)), C(c(c(a(z0, z1)))), C(c(a(z0, z1))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(b(c(c(c(c(z1)))), a(z0, 0)))), C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(c(a(x0, c(a(x1, x2)))))) → c1(C(c(b(c(c(c(c(x2)))), x1))))
C(c(c(a(x0, b(c(a(z0, 0)), 0))))) → c1(C(c(a(0, c(z0)))), C(c(c(b(c(a(z0, 0)), 0)))), C(c(b(c(a(z0, 0)), 0))), C(b(c(a(z0, 0)), 0)))
C(c(c(a(x0, b(c(x1), 0))))) → c1(C(c(c(b(c(x1), 0)))), C(c(b(c(x1), 0))))
K tuples:none
Defined Rule Symbols:

c

Defined Pair Symbols:

C

Compound Symbols:

c3, c1, c2, c1, c1

(15) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace C(c(c(a(x0, a(a(z0, 0), z1))))) → c1(C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))), C(a(a(z0, 0), z1))) by

C(c(c(a(x0, a(a(z0, 0), z1))))) → c1(C(c(c(z0))), C(c(z0)), C(c(a(a(z0, 0), z1))), C(a(a(z0, 0), z1)))
C(c(c(a(x0, a(a(x1, 0), x2))))) → c1

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(a(z0, z1)))) → b(c(c(c(c(z1)))), z0)
c(c(b(c(z0), 0))) → a(0, c(c(a(z0, 0))))
c(c(a(a(z0, 0), z1))) → c(z0)
Tuples:

C(c(a(a(z0, 0), z1))) → c3(C(z0))
C(c(c(a(x0, c(c(a(z0, z1))))))) → c1(C(c(c(b(c(c(c(c(z1)))), z0)))), C(c(c(c(c(a(z0, z1)))))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))))
C(c(c(a(x0, c(b(c(z0), 0)))))) → c1(C(c(c(a(0, c(c(a(z0, 0))))))), C(c(c(c(b(c(z0), 0))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(c(c(z0)))), C(c(c(c(a(a(z0, 0), z1))))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(b(c(x0), 0))) → c2(C(c(a(x0, 0))))
C(c(c(a(x0, a(x1, a(z0, z1)))))) → c1(C(b(c(b(c(c(c(c(z1)))), z0)), x1)), C(c(c(a(x1, a(z0, z1))))), C(c(a(x1, a(z0, z1)))), C(a(x1, a(z0, z1))))
C(c(c(a(x0, a(x1, c(a(z0, z1))))))) → c1(C(b(c(c(b(c(c(c(c(z1)))), z0))), x1)), C(c(c(a(x1, c(a(z0, z1)))))), C(c(a(x1, c(a(z0, z1))))), C(a(x1, c(a(z0, z1)))))
C(c(c(a(x0, a(x1, b(c(z0), 0)))))) → c1(C(b(c(c(a(0, c(c(a(z0, 0)))))), x1)), C(c(c(a(x1, b(c(z0), 0))))), C(c(a(x1, b(c(z0), 0)))), C(a(x1, b(c(z0), 0))))
C(c(c(a(x0, a(x1, a(a(z0, 0), z1)))))) → c1(C(b(c(c(c(z0))), x1)), C(c(c(a(x1, a(a(z0, 0), z1))))), C(c(a(x1, a(a(z0, 0), z1)))), C(a(x1, a(a(z0, 0), z1))))
C(c(c(a(x0, a(x1, c(c(a(z0, z1)))))))) → c1(C(b(c(c(c(b(c(c(c(c(z1)))), z0)))), x1)), C(c(c(a(x1, c(c(a(z0, z1))))))), C(c(a(x1, c(c(a(z0, z1)))))), C(a(x1, c(c(a(z0, z1))))))
C(c(c(a(x0, a(x1, c(b(c(z0), 0))))))) → c1(C(b(c(c(c(a(0, c(c(a(z0, 0))))))), x1)), C(c(c(a(x1, c(b(c(z0), 0)))))), C(c(a(x1, c(b(c(z0), 0))))), C(a(x1, c(b(c(z0), 0)))))
C(c(c(a(x0, a(x1, c(a(a(z0, 0), z1))))))) → c1(C(b(c(c(c(c(z0)))), x1)), C(c(c(a(x1, c(a(a(z0, 0), z1)))))), C(c(a(x1, c(a(a(z0, 0), z1))))), C(a(x1, c(a(a(z0, 0), z1)))))
C(c(c(a(x0, a(x1, x2))))) → c1(C(c(c(a(x1, x2)))), C(c(a(x1, x2))))
C(c(c(a(x0, c(a(z0, z1)))))) → c1(C(c(b(c(c(c(c(z1)))), z0))), C(b(c(c(c(c(z1)))), z0)), C(c(c(a(z0, z1)))), C(c(a(z0, z1))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(b(c(c(c(c(z1)))), a(z0, 0)))), C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(c(a(x0, c(a(x1, x2)))))) → c1(C(c(b(c(c(c(c(x2)))), x1))))
C(c(c(a(x0, b(c(a(z0, 0)), 0))))) → c1(C(c(a(0, c(z0)))), C(c(c(b(c(a(z0, 0)), 0)))), C(c(b(c(a(z0, 0)), 0))), C(b(c(a(z0, 0)), 0)))
C(c(c(a(x0, b(c(x1), 0))))) → c1(C(c(c(b(c(x1), 0)))), C(c(b(c(x1), 0))))
C(c(c(a(x0, a(a(z0, 0), z1))))) → c1(C(c(c(z0))), C(c(z0)), C(c(a(a(z0, 0), z1))), C(a(a(z0, 0), z1)))
C(c(c(a(x0, a(a(x1, 0), x2))))) → c1
S tuples:

C(c(a(a(z0, 0), z1))) → c3(C(z0))
C(c(c(a(x0, c(c(a(z0, z1))))))) → c1(C(c(c(b(c(c(c(c(z1)))), z0)))), C(c(c(c(c(a(z0, z1)))))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))))
C(c(c(a(x0, c(b(c(z0), 0)))))) → c1(C(c(c(a(0, c(c(a(z0, 0))))))), C(c(c(c(b(c(z0), 0))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(c(c(z0)))), C(c(c(c(a(a(z0, 0), z1))))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(b(c(x0), 0))) → c2(C(c(a(x0, 0))))
C(c(c(a(x0, a(x1, a(z0, z1)))))) → c1(C(b(c(b(c(c(c(c(z1)))), z0)), x1)), C(c(c(a(x1, a(z0, z1))))), C(c(a(x1, a(z0, z1)))), C(a(x1, a(z0, z1))))
C(c(c(a(x0, a(x1, c(a(z0, z1))))))) → c1(C(b(c(c(b(c(c(c(c(z1)))), z0))), x1)), C(c(c(a(x1, c(a(z0, z1)))))), C(c(a(x1, c(a(z0, z1))))), C(a(x1, c(a(z0, z1)))))
C(c(c(a(x0, a(x1, b(c(z0), 0)))))) → c1(C(b(c(c(a(0, c(c(a(z0, 0)))))), x1)), C(c(c(a(x1, b(c(z0), 0))))), C(c(a(x1, b(c(z0), 0)))), C(a(x1, b(c(z0), 0))))
C(c(c(a(x0, a(x1, a(a(z0, 0), z1)))))) → c1(C(b(c(c(c(z0))), x1)), C(c(c(a(x1, a(a(z0, 0), z1))))), C(c(a(x1, a(a(z0, 0), z1)))), C(a(x1, a(a(z0, 0), z1))))
C(c(c(a(x0, a(x1, c(c(a(z0, z1)))))))) → c1(C(b(c(c(c(b(c(c(c(c(z1)))), z0)))), x1)), C(c(c(a(x1, c(c(a(z0, z1))))))), C(c(a(x1, c(c(a(z0, z1)))))), C(a(x1, c(c(a(z0, z1))))))
C(c(c(a(x0, a(x1, c(b(c(z0), 0))))))) → c1(C(b(c(c(c(a(0, c(c(a(z0, 0))))))), x1)), C(c(c(a(x1, c(b(c(z0), 0)))))), C(c(a(x1, c(b(c(z0), 0))))), C(a(x1, c(b(c(z0), 0)))))
C(c(c(a(x0, a(x1, c(a(a(z0, 0), z1))))))) → c1(C(b(c(c(c(c(z0)))), x1)), C(c(c(a(x1, c(a(a(z0, 0), z1)))))), C(c(a(x1, c(a(a(z0, 0), z1))))), C(a(x1, c(a(a(z0, 0), z1)))))
C(c(c(a(x0, a(x1, x2))))) → c1(C(c(c(a(x1, x2)))), C(c(a(x1, x2))))
C(c(c(a(x0, c(a(z0, z1)))))) → c1(C(c(b(c(c(c(c(z1)))), z0))), C(b(c(c(c(c(z1)))), z0)), C(c(c(a(z0, z1)))), C(c(a(z0, z1))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(b(c(c(c(c(z1)))), a(z0, 0)))), C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(c(a(x0, c(a(x1, x2)))))) → c1(C(c(b(c(c(c(c(x2)))), x1))))
C(c(c(a(x0, b(c(a(z0, 0)), 0))))) → c1(C(c(a(0, c(z0)))), C(c(c(b(c(a(z0, 0)), 0)))), C(c(b(c(a(z0, 0)), 0))), C(b(c(a(z0, 0)), 0)))
C(c(c(a(x0, b(c(x1), 0))))) → c1(C(c(c(b(c(x1), 0)))), C(c(b(c(x1), 0))))
C(c(c(a(x0, a(a(z0, 0), z1))))) → c1(C(c(c(z0))), C(c(z0)), C(c(a(a(z0, 0), z1))), C(a(a(z0, 0), z1)))
C(c(c(a(x0, a(a(x1, 0), x2))))) → c1
K tuples:none
Defined Rule Symbols:

c

Defined Pair Symbols:

C

Compound Symbols:

c3, c1, c2, c1, c1, c1

(17) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

C(c(c(a(x0, a(a(x1, 0), x2))))) → c1

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(a(z0, z1)))) → b(c(c(c(c(z1)))), z0)
c(c(b(c(z0), 0))) → a(0, c(c(a(z0, 0))))
c(c(a(a(z0, 0), z1))) → c(z0)
Tuples:

C(c(a(a(z0, 0), z1))) → c3(C(z0))
C(c(c(a(x0, c(c(a(z0, z1))))))) → c1(C(c(c(b(c(c(c(c(z1)))), z0)))), C(c(c(c(c(a(z0, z1)))))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))))
C(c(c(a(x0, c(b(c(z0), 0)))))) → c1(C(c(c(a(0, c(c(a(z0, 0))))))), C(c(c(c(b(c(z0), 0))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(c(c(z0)))), C(c(c(c(a(a(z0, 0), z1))))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(b(c(x0), 0))) → c2(C(c(a(x0, 0))))
C(c(c(a(x0, a(x1, a(z0, z1)))))) → c1(C(b(c(b(c(c(c(c(z1)))), z0)), x1)), C(c(c(a(x1, a(z0, z1))))), C(c(a(x1, a(z0, z1)))), C(a(x1, a(z0, z1))))
C(c(c(a(x0, a(x1, c(a(z0, z1))))))) → c1(C(b(c(c(b(c(c(c(c(z1)))), z0))), x1)), C(c(c(a(x1, c(a(z0, z1)))))), C(c(a(x1, c(a(z0, z1))))), C(a(x1, c(a(z0, z1)))))
C(c(c(a(x0, a(x1, b(c(z0), 0)))))) → c1(C(b(c(c(a(0, c(c(a(z0, 0)))))), x1)), C(c(c(a(x1, b(c(z0), 0))))), C(c(a(x1, b(c(z0), 0)))), C(a(x1, b(c(z0), 0))))
C(c(c(a(x0, a(x1, a(a(z0, 0), z1)))))) → c1(C(b(c(c(c(z0))), x1)), C(c(c(a(x1, a(a(z0, 0), z1))))), C(c(a(x1, a(a(z0, 0), z1)))), C(a(x1, a(a(z0, 0), z1))))
C(c(c(a(x0, a(x1, c(c(a(z0, z1)))))))) → c1(C(b(c(c(c(b(c(c(c(c(z1)))), z0)))), x1)), C(c(c(a(x1, c(c(a(z0, z1))))))), C(c(a(x1, c(c(a(z0, z1)))))), C(a(x1, c(c(a(z0, z1))))))
C(c(c(a(x0, a(x1, c(b(c(z0), 0))))))) → c1(C(b(c(c(c(a(0, c(c(a(z0, 0))))))), x1)), C(c(c(a(x1, c(b(c(z0), 0)))))), C(c(a(x1, c(b(c(z0), 0))))), C(a(x1, c(b(c(z0), 0)))))
C(c(c(a(x0, a(x1, c(a(a(z0, 0), z1))))))) → c1(C(b(c(c(c(c(z0)))), x1)), C(c(c(a(x1, c(a(a(z0, 0), z1)))))), C(c(a(x1, c(a(a(z0, 0), z1))))), C(a(x1, c(a(a(z0, 0), z1)))))
C(c(c(a(x0, a(x1, x2))))) → c1(C(c(c(a(x1, x2)))), C(c(a(x1, x2))))
C(c(c(a(x0, c(a(z0, z1)))))) → c1(C(c(b(c(c(c(c(z1)))), z0))), C(b(c(c(c(c(z1)))), z0)), C(c(c(a(z0, z1)))), C(c(a(z0, z1))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(b(c(c(c(c(z1)))), a(z0, 0)))), C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(c(a(x0, c(a(x1, x2)))))) → c1(C(c(b(c(c(c(c(x2)))), x1))))
C(c(c(a(x0, b(c(a(z0, 0)), 0))))) → c1(C(c(a(0, c(z0)))), C(c(c(b(c(a(z0, 0)), 0)))), C(c(b(c(a(z0, 0)), 0))), C(b(c(a(z0, 0)), 0)))
C(c(c(a(x0, b(c(x1), 0))))) → c1(C(c(c(b(c(x1), 0)))), C(c(b(c(x1), 0))))
C(c(c(a(x0, a(a(z0, 0), z1))))) → c1(C(c(c(z0))), C(c(z0)), C(c(a(a(z0, 0), z1))), C(a(a(z0, 0), z1)))
S tuples:

C(c(a(a(z0, 0), z1))) → c3(C(z0))
C(c(c(a(x0, c(c(a(z0, z1))))))) → c1(C(c(c(b(c(c(c(c(z1)))), z0)))), C(c(c(c(c(a(z0, z1)))))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1)))))
C(c(c(a(x0, c(b(c(z0), 0)))))) → c1(C(c(c(a(0, c(c(a(z0, 0))))))), C(c(c(c(b(c(z0), 0))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(c(c(z0)))), C(c(c(c(a(a(z0, 0), z1))))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(b(c(x0), 0))) → c2(C(c(a(x0, 0))))
C(c(c(a(x0, a(x1, a(z0, z1)))))) → c1(C(b(c(b(c(c(c(c(z1)))), z0)), x1)), C(c(c(a(x1, a(z0, z1))))), C(c(a(x1, a(z0, z1)))), C(a(x1, a(z0, z1))))
C(c(c(a(x0, a(x1, c(a(z0, z1))))))) → c1(C(b(c(c(b(c(c(c(c(z1)))), z0))), x1)), C(c(c(a(x1, c(a(z0, z1)))))), C(c(a(x1, c(a(z0, z1))))), C(a(x1, c(a(z0, z1)))))
C(c(c(a(x0, a(x1, b(c(z0), 0)))))) → c1(C(b(c(c(a(0, c(c(a(z0, 0)))))), x1)), C(c(c(a(x1, b(c(z0), 0))))), C(c(a(x1, b(c(z0), 0)))), C(a(x1, b(c(z0), 0))))
C(c(c(a(x0, a(x1, a(a(z0, 0), z1)))))) → c1(C(b(c(c(c(z0))), x1)), C(c(c(a(x1, a(a(z0, 0), z1))))), C(c(a(x1, a(a(z0, 0), z1)))), C(a(x1, a(a(z0, 0), z1))))
C(c(c(a(x0, a(x1, c(c(a(z0, z1)))))))) → c1(C(b(c(c(c(b(c(c(c(c(z1)))), z0)))), x1)), C(c(c(a(x1, c(c(a(z0, z1))))))), C(c(a(x1, c(c(a(z0, z1)))))), C(a(x1, c(c(a(z0, z1))))))
C(c(c(a(x0, a(x1, c(b(c(z0), 0))))))) → c1(C(b(c(c(c(a(0, c(c(a(z0, 0))))))), x1)), C(c(c(a(x1, c(b(c(z0), 0)))))), C(c(a(x1, c(b(c(z0), 0))))), C(a(x1, c(b(c(z0), 0)))))
C(c(c(a(x0, a(x1, c(a(a(z0, 0), z1))))))) → c1(C(b(c(c(c(c(z0)))), x1)), C(c(c(a(x1, c(a(a(z0, 0), z1)))))), C(c(a(x1, c(a(a(z0, 0), z1))))), C(a(x1, c(a(a(z0, 0), z1)))))
C(c(c(a(x0, a(x1, x2))))) → c1(C(c(c(a(x1, x2)))), C(c(a(x1, x2))))
C(c(c(a(x0, c(a(z0, z1)))))) → c1(C(c(b(c(c(c(c(z1)))), z0))), C(b(c(c(c(c(z1)))), z0)), C(c(c(a(z0, z1)))), C(c(a(z0, z1))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(b(c(c(c(c(z1)))), a(z0, 0)))), C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(c(a(x0, c(a(x1, x2)))))) → c1(C(c(b(c(c(c(c(x2)))), x1))))
C(c(c(a(x0, b(c(a(z0, 0)), 0))))) → c1(C(c(a(0, c(z0)))), C(c(c(b(c(a(z0, 0)), 0)))), C(c(b(c(a(z0, 0)), 0))), C(b(c(a(z0, 0)), 0)))
C(c(c(a(x0, b(c(x1), 0))))) → c1(C(c(c(b(c(x1), 0)))), C(c(b(c(x1), 0))))
C(c(c(a(x0, a(a(z0, 0), z1))))) → c1(C(c(c(z0))), C(c(z0)), C(c(a(a(z0, 0), z1))), C(a(a(z0, 0), z1)))
K tuples:none
Defined Rule Symbols:

c

Defined Pair Symbols:

C

Compound Symbols:

c3, c1, c2, c1, c1

(19) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace C(c(c(a(x0, c(c(a(z0, z1))))))) → c1(C(c(c(b(c(c(c(c(z1)))), z0)))), C(c(c(c(c(a(z0, z1)))))), C(c(c(c(a(z0, z1))))), C(c(c(a(z0, z1))))) by

C(c(c(a(x0, c(c(a(0, x2))))))) → c1(C(a(0, c(c(a(c(c(c(x2))), 0))))), C(c(c(c(c(a(0, x2)))))), C(c(c(c(a(0, x2))))), C(c(c(a(0, x2)))))
C(c(c(a(x0, c(c(a(x1, a(z0, z1)))))))) → c1(C(c(c(b(c(b(c(c(c(c(z1)))), z0)), x1)))), C(c(c(c(c(a(x1, a(z0, z1))))))), C(c(c(c(a(x1, a(z0, z1)))))), C(c(c(a(x1, a(z0, z1))))))
C(c(c(a(x0, c(c(a(x1, b(c(z0), 0)))))))) → c1(C(c(c(b(c(c(a(0, c(c(a(z0, 0)))))), x1)))), C(c(c(c(c(a(x1, b(c(z0), 0))))))), C(c(c(c(a(x1, b(c(z0), 0)))))), C(c(c(a(x1, b(c(z0), 0))))))
C(c(c(a(x0, c(c(a(x1, c(a(z0, z1))))))))) → c1(C(c(c(b(c(c(b(c(c(c(c(z1)))), z0))), x1)))), C(c(c(c(c(a(x1, c(a(z0, z1)))))))), C(c(c(c(a(x1, c(a(z0, z1))))))), C(c(c(a(x1, c(a(z0, z1)))))))
C(c(c(a(x0, c(c(a(x1, a(a(z0, 0), z1)))))))) → c1(C(c(c(b(c(c(c(z0))), x1)))), C(c(c(c(c(a(x1, a(a(z0, 0), z1))))))), C(c(c(c(a(x1, a(a(z0, 0), z1)))))), C(c(c(a(x1, a(a(z0, 0), z1))))))
C(c(c(a(x0, c(c(a(x1, c(b(c(z0), 0))))))))) → c1(C(c(c(b(c(c(c(a(0, c(c(a(z0, 0))))))), x1)))), C(c(c(c(c(a(x1, c(b(c(z0), 0)))))))), C(c(c(c(a(x1, c(b(c(z0), 0))))))), C(c(c(a(x1, c(b(c(z0), 0)))))))
C(c(c(a(x0, c(c(a(x1, c(c(a(z0, z1)))))))))) → c1(C(c(c(b(c(c(c(b(c(c(c(c(z1)))), z0)))), x1)))), C(c(c(c(c(a(x1, c(c(a(z0, z1))))))))), C(c(c(c(a(x1, c(c(a(z0, z1)))))))), C(c(c(a(x1, c(c(a(z0, z1))))))))
C(c(c(a(x0, c(c(a(x1, c(a(a(z0, 0), z1))))))))) → c1(C(c(c(b(c(c(c(c(z0)))), x1)))), C(c(c(c(c(a(x1, c(a(a(z0, 0), z1)))))))), C(c(c(c(a(x1, c(a(a(z0, 0), z1))))))), C(c(c(a(x1, c(a(a(z0, 0), z1)))))))
C(c(c(a(x0, c(c(a(x1, x2))))))) → c1(C(c(c(c(c(a(x1, x2)))))), C(c(c(c(a(x1, x2))))))

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(a(z0, z1)))) → b(c(c(c(c(z1)))), z0)
c(c(b(c(z0), 0))) → a(0, c(c(a(z0, 0))))
c(c(a(a(z0, 0), z1))) → c(z0)
Tuples:

C(c(a(a(z0, 0), z1))) → c3(C(z0))
C(c(c(a(x0, c(b(c(z0), 0)))))) → c1(C(c(c(a(0, c(c(a(z0, 0))))))), C(c(c(c(b(c(z0), 0))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(c(c(z0)))), C(c(c(c(a(a(z0, 0), z1))))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(b(c(x0), 0))) → c2(C(c(a(x0, 0))))
C(c(c(a(x0, a(x1, a(z0, z1)))))) → c1(C(b(c(b(c(c(c(c(z1)))), z0)), x1)), C(c(c(a(x1, a(z0, z1))))), C(c(a(x1, a(z0, z1)))), C(a(x1, a(z0, z1))))
C(c(c(a(x0, a(x1, c(a(z0, z1))))))) → c1(C(b(c(c(b(c(c(c(c(z1)))), z0))), x1)), C(c(c(a(x1, c(a(z0, z1)))))), C(c(a(x1, c(a(z0, z1))))), C(a(x1, c(a(z0, z1)))))
C(c(c(a(x0, a(x1, b(c(z0), 0)))))) → c1(C(b(c(c(a(0, c(c(a(z0, 0)))))), x1)), C(c(c(a(x1, b(c(z0), 0))))), C(c(a(x1, b(c(z0), 0)))), C(a(x1, b(c(z0), 0))))
C(c(c(a(x0, a(x1, a(a(z0, 0), z1)))))) → c1(C(b(c(c(c(z0))), x1)), C(c(c(a(x1, a(a(z0, 0), z1))))), C(c(a(x1, a(a(z0, 0), z1)))), C(a(x1, a(a(z0, 0), z1))))
C(c(c(a(x0, a(x1, c(c(a(z0, z1)))))))) → c1(C(b(c(c(c(b(c(c(c(c(z1)))), z0)))), x1)), C(c(c(a(x1, c(c(a(z0, z1))))))), C(c(a(x1, c(c(a(z0, z1)))))), C(a(x1, c(c(a(z0, z1))))))
C(c(c(a(x0, a(x1, c(b(c(z0), 0))))))) → c1(C(b(c(c(c(a(0, c(c(a(z0, 0))))))), x1)), C(c(c(a(x1, c(b(c(z0), 0)))))), C(c(a(x1, c(b(c(z0), 0))))), C(a(x1, c(b(c(z0), 0)))))
C(c(c(a(x0, a(x1, c(a(a(z0, 0), z1))))))) → c1(C(b(c(c(c(c(z0)))), x1)), C(c(c(a(x1, c(a(a(z0, 0), z1)))))), C(c(a(x1, c(a(a(z0, 0), z1))))), C(a(x1, c(a(a(z0, 0), z1)))))
C(c(c(a(x0, a(x1, x2))))) → c1(C(c(c(a(x1, x2)))), C(c(a(x1, x2))))
C(c(c(a(x0, c(a(z0, z1)))))) → c1(C(c(b(c(c(c(c(z1)))), z0))), C(b(c(c(c(c(z1)))), z0)), C(c(c(a(z0, z1)))), C(c(a(z0, z1))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(b(c(c(c(c(z1)))), a(z0, 0)))), C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(c(a(x0, c(a(x1, x2)))))) → c1(C(c(b(c(c(c(c(x2)))), x1))))
C(c(c(a(x0, b(c(a(z0, 0)), 0))))) → c1(C(c(a(0, c(z0)))), C(c(c(b(c(a(z0, 0)), 0)))), C(c(b(c(a(z0, 0)), 0))), C(b(c(a(z0, 0)), 0)))
C(c(c(a(x0, b(c(x1), 0))))) → c1(C(c(c(b(c(x1), 0)))), C(c(b(c(x1), 0))))
C(c(c(a(x0, a(a(z0, 0), z1))))) → c1(C(c(c(z0))), C(c(z0)), C(c(a(a(z0, 0), z1))), C(a(a(z0, 0), z1)))
C(c(c(a(x0, c(c(a(0, x2))))))) → c1(C(a(0, c(c(a(c(c(c(x2))), 0))))), C(c(c(c(c(a(0, x2)))))), C(c(c(c(a(0, x2))))), C(c(c(a(0, x2)))))
C(c(c(a(x0, c(c(a(x1, a(z0, z1)))))))) → c1(C(c(c(b(c(b(c(c(c(c(z1)))), z0)), x1)))), C(c(c(c(c(a(x1, a(z0, z1))))))), C(c(c(c(a(x1, a(z0, z1)))))), C(c(c(a(x1, a(z0, z1))))))
C(c(c(a(x0, c(c(a(x1, b(c(z0), 0)))))))) → c1(C(c(c(b(c(c(a(0, c(c(a(z0, 0)))))), x1)))), C(c(c(c(c(a(x1, b(c(z0), 0))))))), C(c(c(c(a(x1, b(c(z0), 0)))))), C(c(c(a(x1, b(c(z0), 0))))))
C(c(c(a(x0, c(c(a(x1, c(a(z0, z1))))))))) → c1(C(c(c(b(c(c(b(c(c(c(c(z1)))), z0))), x1)))), C(c(c(c(c(a(x1, c(a(z0, z1)))))))), C(c(c(c(a(x1, c(a(z0, z1))))))), C(c(c(a(x1, c(a(z0, z1)))))))
C(c(c(a(x0, c(c(a(x1, a(a(z0, 0), z1)))))))) → c1(C(c(c(b(c(c(c(z0))), x1)))), C(c(c(c(c(a(x1, a(a(z0, 0), z1))))))), C(c(c(c(a(x1, a(a(z0, 0), z1)))))), C(c(c(a(x1, a(a(z0, 0), z1))))))
C(c(c(a(x0, c(c(a(x1, c(b(c(z0), 0))))))))) → c1(C(c(c(b(c(c(c(a(0, c(c(a(z0, 0))))))), x1)))), C(c(c(c(c(a(x1, c(b(c(z0), 0)))))))), C(c(c(c(a(x1, c(b(c(z0), 0))))))), C(c(c(a(x1, c(b(c(z0), 0)))))))
C(c(c(a(x0, c(c(a(x1, c(c(a(z0, z1)))))))))) → c1(C(c(c(b(c(c(c(b(c(c(c(c(z1)))), z0)))), x1)))), C(c(c(c(c(a(x1, c(c(a(z0, z1))))))))), C(c(c(c(a(x1, c(c(a(z0, z1)))))))), C(c(c(a(x1, c(c(a(z0, z1))))))))
C(c(c(a(x0, c(c(a(x1, c(a(a(z0, 0), z1))))))))) → c1(C(c(c(b(c(c(c(c(z0)))), x1)))), C(c(c(c(c(a(x1, c(a(a(z0, 0), z1)))))))), C(c(c(c(a(x1, c(a(a(z0, 0), z1))))))), C(c(c(a(x1, c(a(a(z0, 0), z1)))))))
C(c(c(a(x0, c(c(a(x1, x2))))))) → c1(C(c(c(c(c(a(x1, x2)))))), C(c(c(c(a(x1, x2))))))
S tuples:

C(c(a(a(z0, 0), z1))) → c3(C(z0))
C(c(c(a(x0, c(b(c(z0), 0)))))) → c1(C(c(c(a(0, c(c(a(z0, 0))))))), C(c(c(c(b(c(z0), 0))))), C(c(c(b(c(z0), 0)))), C(c(b(c(z0), 0))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(c(c(z0)))), C(c(c(c(a(a(z0, 0), z1))))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(b(c(x0), 0))) → c2(C(c(a(x0, 0))))
C(c(c(a(x0, a(x1, a(z0, z1)))))) → c1(C(b(c(b(c(c(c(c(z1)))), z0)), x1)), C(c(c(a(x1, a(z0, z1))))), C(c(a(x1, a(z0, z1)))), C(a(x1, a(z0, z1))))
C(c(c(a(x0, a(x1, c(a(z0, z1))))))) → c1(C(b(c(c(b(c(c(c(c(z1)))), z0))), x1)), C(c(c(a(x1, c(a(z0, z1)))))), C(c(a(x1, c(a(z0, z1))))), C(a(x1, c(a(z0, z1)))))
C(c(c(a(x0, a(x1, b(c(z0), 0)))))) → c1(C(b(c(c(a(0, c(c(a(z0, 0)))))), x1)), C(c(c(a(x1, b(c(z0), 0))))), C(c(a(x1, b(c(z0), 0)))), C(a(x1, b(c(z0), 0))))
C(c(c(a(x0, a(x1, a(a(z0, 0), z1)))))) → c1(C(b(c(c(c(z0))), x1)), C(c(c(a(x1, a(a(z0, 0), z1))))), C(c(a(x1, a(a(z0, 0), z1)))), C(a(x1, a(a(z0, 0), z1))))
C(c(c(a(x0, a(x1, c(c(a(z0, z1)))))))) → c1(C(b(c(c(c(b(c(c(c(c(z1)))), z0)))), x1)), C(c(c(a(x1, c(c(a(z0, z1))))))), C(c(a(x1, c(c(a(z0, z1)))))), C(a(x1, c(c(a(z0, z1))))))
C(c(c(a(x0, a(x1, c(b(c(z0), 0))))))) → c1(C(b(c(c(c(a(0, c(c(a(z0, 0))))))), x1)), C(c(c(a(x1, c(b(c(z0), 0)))))), C(c(a(x1, c(b(c(z0), 0))))), C(a(x1, c(b(c(z0), 0)))))
C(c(c(a(x0, a(x1, c(a(a(z0, 0), z1))))))) → c1(C(b(c(c(c(c(z0)))), x1)), C(c(c(a(x1, c(a(a(z0, 0), z1)))))), C(c(a(x1, c(a(a(z0, 0), z1))))), C(a(x1, c(a(a(z0, 0), z1)))))
C(c(c(a(x0, a(x1, x2))))) → c1(C(c(c(a(x1, x2)))), C(c(a(x1, x2))))
C(c(c(a(x0, c(a(z0, z1)))))) → c1(C(c(b(c(c(c(c(z1)))), z0))), C(b(c(c(c(c(z1)))), z0)), C(c(c(a(z0, z1)))), C(c(a(z0, z1))))
C(c(c(a(x0, c(a(a(z0, 0), z1)))))) → c1(C(c(b(c(c(c(c(z1)))), a(z0, 0)))), C(c(c(z0))), C(c(c(a(a(z0, 0), z1)))), C(c(a(a(z0, 0), z1))))
C(c(c(a(x0, c(a(x1, x2)))))) → c1(C(c(b(c(c(c(c(x2)))), x1))))
C(c(c(a(x0, b(c(a(z0, 0)), 0))))) → c1(C(c(a(0, c(z0)))), C(c(c(b(c(a(z0, 0)), 0)))), C(c(b(c(a(z0, 0)), 0))), C(b(c(a(z0, 0)), 0)))
C(c(c(a(x0, b(c(x1), 0))))) → c1(C(c(c(b(c(x1), 0)))), C(c(b(c(x1), 0))))
C(c(c(a(x0, a(a(z0, 0), z1))))) → c1(C(c(c(z0))), C(c(z0)), C(c(a(a(z0, 0), z1))), C(a(a(z0, 0), z1)))
C(c(c(a(x0, c(c(a(0, x2))))))) → c1(C(a(0, c(c(a(c(c(c(x2))), 0))))), C(c(c(c(c(a(0, x2)))))), C(c(c(c(a(0, x2))))), C(c(c(a(0, x2)))))
C(c(c(a(x0, c(c(a(x1, a(z0, z1)))))))) → c1(C(c(c(b(c(b(c(c(c(c(z1)))), z0)), x1)))), C(c(c(c(c(a(x1, a(z0, z1))))))), C(c(c(c(a(x1, a(z0, z1)))))), C(c(c(a(x1, a(z0, z1))))))
C(c(c(a(x0, c(c(a(x1, b(c(z0), 0)))))))) → c1(C(c(c(b(c(c(a(0, c(c(a(z0, 0)))))), x1)))), C(c(c(c(c(a(x1, b(c(z0), 0))))))), C(c(c(c(a(x1, b(c(z0), 0)))))), C(c(c(a(x1, b(c(z0), 0))))))
C(c(c(a(x0, c(c(a(x1, c(a(z0, z1))))))))) → c1(C(c(c(b(c(c(b(c(c(c(c(z1)))), z0))), x1)))), C(c(c(c(c(a(x1, c(a(z0, z1)))))))), C(c(c(c(a(x1, c(a(z0, z1))))))), C(c(c(a(x1, c(a(z0, z1)))))))
C(c(c(a(x0, c(c(a(x1, a(a(z0, 0), z1)))))))) → c1(C(c(c(b(c(c(c(z0))), x1)))), C(c(c(c(c(a(x1, a(a(z0, 0), z1))))))), C(c(c(c(a(x1, a(a(z0, 0), z1)))))), C(c(c(a(x1, a(a(z0, 0), z1))))))
C(c(c(a(x0, c(c(a(x1, c(b(c(z0), 0))))))))) → c1(C(c(c(b(c(c(c(a(0, c(c(a(z0, 0))))))), x1)))), C(c(c(c(c(a(x1, c(b(c(z0), 0)))))))), C(c(c(c(a(x1, c(b(c(z0), 0))))))), C(c(c(a(x1, c(b(c(z0), 0)))))))
C(c(c(a(x0, c(c(a(x1, c(c(a(z0, z1)))))))))) → c1(C(c(c(b(c(c(c(b(c(c(c(c(z1)))), z0)))), x1)))), C(c(c(c(c(a(x1, c(c(a(z0, z1))))))))), C(c(c(c(a(x1, c(c(a(z0, z1)))))))), C(c(c(a(x1, c(c(a(z0, z1))))))))
C(c(c(a(x0, c(c(a(x1, c(a(a(z0, 0), z1))))))))) → c1(C(c(c(b(c(c(c(c(z0)))), x1)))), C(c(c(c(c(a(x1, c(a(a(z0, 0), z1)))))))), C(c(c(c(a(x1, c(a(a(z0, 0), z1))))))), C(c(c(a(x1, c(a(a(z0, 0), z1)))))))
C(c(c(a(x0, c(c(a(x1, x2))))))) → c1(C(c(c(c(c(a(x1, x2)))))), C(c(c(c(a(x1, x2))))))
K tuples:none
Defined Rule Symbols:

c

Defined Pair Symbols:

C

Compound Symbols:

c3, c1, c2, c1, c1

(21) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 0.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1]
transitions:
a0(0, 0) → 0
b0(0, 0) → 0
00() → 0
c0(0) → 1

(22) BOUNDS(O(1), O(n^1))